i:Id, A, B:MsgA. @i: A  @i: B  A  B 

latex

Definitions	P  Q, SQType(T), {T}, False, @i: A, D1  D2, M(i), P  Q, if b t else f fi, Unit, P  Q, P & Q, a = b, , b, Id, A, Prop, b, M1  M2, MsgA, x:A. B(x), P  Q, t  T,
Lemmas	ma-empty wf, ma-sub weakening, assert wf, not wf, bnot wf, bool wf, eq id wf, assert-eq-id, not functionality wrt iff, assert of bnot, iff transitivity, eqff to assert, eqtt to assert, ma-sub wf, Id wf, ifthenelse wf, msga wf, bool sq, bool cases